package tr.edu.ege.kipler.satisfiability.completion.rules;

import tr.edu.ege.kipler.satisfiability.ReasonerException;
import tr.edu.ege.kipler.satisfiability.container.World;
import tr.edu.ege.kipler.satisfiability.container.WorldConstraintSystem;

/**
 * The concrete implementations of this abstract class are the tableau rules
 * that modify a world constraint system.
 * 
 * @author İnanç Seylan
 * 
 */
public abstract class CompletionRule {
	/**
	 * The world constraint system containing the world that this tableau rule
	 * will be applied
	 */
	private WorldConstraintSystem wcs;

	/**
	 * The world to whose formulae this tableau rule is to be applied
	 */
	private World world;

	public CompletionRule() {
		
	}
	
	public CompletionRule(WorldConstraintSystem wcs, World world) {
		setWcs(wcs);
		setWorld(world);
	}
 	
	/**
	 * The concrete implementations of this method apply the logic behind that
	 * concrete tableau rule.
	 */
	public abstract void apply() throws ReasonerException;

	public abstract boolean isApplied();
	
	/**
	 * @return the world constraint system that this rule modifies.
	 */
	public WorldConstraintSystem getWcs() {
		return wcs;
	}

	/**
	 * Sets the world constraint system that this rule modifies.
	 * 
	 * @param wcs
	 *            The world constraint system
	 */
	public void setWcs(WorldConstraintSystem wcs) {
		this.wcs = wcs;
	}

	/**
	 * @return the world to which this tableau rule is to be applied.
	 */
	public World getWorld() {
		return world;
	}

	/**
	 * @param world
	 *            The world to set.
	 */
	public void setWorld(World world) {
		this.world = world;
	}

}
